FDL - Nuprl Lemma : fpf-sub

Nuprl Lemma : fpf-sub_transitivity

11,40

A:Type, B:(A

Type), eq:EqDecider(A), f,g,h:fpf(A; a.B(a)).
fpf-sub(A; a.B(a); eq; f; g)

fpf-sub(A; a.B(a); eq; g; h)

fpf-sub(A; a.B(a); eq; f; h)

Definitions x:A. B(x), x(s), P Q, fpf-sub(A; a.B(a); eq; f; g), A c B, t T, x. t(x), prop{i:l}

Lemmas assert wf, fpf-dom wf, fpf-trivial-subtype-top, fpf-sub wf, fpf wf, deq wf

Definitions	x:A. B(x), x(s), P Q, fpf-sub(A; a.B(a); eq; f; g), A c B, t T, x. t(x), prop{i:l}
Lemmas	assert wf, fpf-dom wf, fpf-trivial-subtype-top, fpf-sub wf, fpf wf, deq wf